package GSR.web;


import static constants.GTextbookConstants.language;

import java.io.File;
import java.util.Vector;

import javax.swing.JOptionPane;

import com.maplesoft.externalcall.MapleException;
import com.maplesoft.openmaple.Engine;
import com.maplesoft.openmaple.EngineCallBacksDefault;

import ui.view.LangWarningPane;
import automatica.TypeIndex;
import automatica.autoprove.Map2GEOTHER;
import automatica.autoprove.MapleLink;
import automatica.explain.Transform;
import automatica.parser.Parser;
/**
 * @author Xiaoyu E-mail: franknewchen@gamil.com
 * @version 创建时间：Nov 14, 2012 3:51:32 PM
 * 类说明
/**
 * @author Franknew
 *
 */
public class Prove {

	  public Prove(String name, String statement, String prover, Engine engine, CallBacks callback) {
		  	//initialize the primitive words used in the system
		    constants.GTextbookConstants.initialReserveWords();
			
			//int count = 1;
			
			/*
		    String PROBLEM_XML = "D://return/problem.xml";
		    String SCRIPT_XML = "D://return/script4prove.xml";
		    String SCRIPT_TXT = "D://return/script4prove.txt";
		    String Transformation_Result = "D://return/transformationResult.xml";
		    String Mapping_Result = "D://return/result4prove.txt";
		    String Proof_Result = "D://return/proof"+name+".html";
		    */
			/*String PROBLEM_XML = "../GDL/problem.xml";
		    String SCRIPT_XML = "../GDL/script4prove.xml";
		    String SCRIPT_TXT = "../GDL/script4prove.txt";
		    String Transformation_Result = "../GDL/transformationResult.xml";
		    String Mapping_Result = "../GDL/result4prove.txt";
		    String Proof_Result = "D://return/proof"+name+".html";*/
		    
		    String PROBLEM_XML = "./result/problem.xml";
		    String SCRIPT_XML = "./result/script4prove.xml";
		    String SCRIPT_TXT = "./result/script4prove.txt";
		    String Transformation_Result = "./result/transformationResult.xml";
		    String Mapping_Result = "./result/result4prove.txt";
		    String Proof_Result = "./result/proof"+name+".html";
			
			
		    String author = "Administrator";
		    
		    
			/*parse the statement
			 * ...,...,...,...<=>...
			 * ...,...,...,...=>...
			 */

		    String text = Utility.getFormalString4Multiple(statement, name, "Prove");
		    
		    
		    
		    /*Proposition(N,T,configuration(),...)
			 * 
			 * Problem(N,T,configuration(),...)
		    */
			Parser p = new Parser(text, new File(PROBLEM_XML));
			p.parse(constants.GTextbookConstants.Assertion,author,null);
		    
		    File scriptFile = new File(SCRIPT_XML);
			//if(!scriptFile.exists()){
			Parser pd = new Parser(new File(SCRIPT_TXT), scriptFile);
			pd.parse(constants.GTextbookConstants.Definition,author,null);
			//}
		    
		    //initial the index
		    TypeIndex index = new TypeIndex();
	    	index.initialize(SCRIPT_XML);
			
	    	
			Transform.transform(index,PROBLEM_XML,Transformation_Result);
			//String output = tempDirectory.toString()+"/resultOut.xml";
			//show(defaultDirectory+"/GSR result/result.xml",output,resultBrowser,"proposition");
			
			//generate the string for GEOTHER
			Map2GEOTHER normalForm = new Map2GEOTHER(Transformation_Result,"./result/xsl/xml2string4prove.xsl",Mapping_Result);                                    
			
		
			for(int i = 0; i < normalForm.getPredicate4GEOTHER().size()-1; i++){
				nativeRepresentations.append(normalForm.getPredicate4GEOTHER().get(i)+"\n and \n");
			}
			nativeRepresentations.append(normalForm.getPredicate4GEOTHER().get(normalForm.getPredicate4GEOTHER().size()-1));
			
			
			 this.callback = callback;
			 this.engine = engine;
			//map to geother
			for(int i = 0; i < normalForm.getPredicate4GEOTHER().size(); i++){
				//MapleLink prove = new MapleLink(engine, "PROBLEM_" + count + (i+1==1?null:"_"+i+1),normalForm.getPredicate4GEOTHER().get(i));
				new MapleLink(engine, "PROBLEM_" + name + "_" + (i+1),normalForm.getPredicate4GEOTHER().get(i));	
			}
			//count++;
			
			
			
			
			htmlOfProof =  "<html><head><style type='text/css'> span.text {color:black; font-family:verdana;font-size:90%;} span.status{color:rgb(160,160,160);}</style></head><body><div>" + callback.getOutput() + "</div>" +
					"<script type='text/javascript'>document.scroll(0,document.body.scrollHeight);</script></body></html>";
			
			/*
			File proofFile = new File(Proof_Result);
			if(proofFile.exists()){
				proofFile.delete();
			}
			ui.Utility.saveFile(null,htmlOfProof, proofFile);
			*/
			//System.out.println(text);
			
			
	  }
	  
		
	  
	  
	  
	  /**
	 * @return the engine
	 */
	public Engine getEngine() {
		return engine;
	}





	/**
	 * @param engine the engine to set
	 */
	public void setEngine(Engine engine) {
		this.engine = engine;
	}





	
	  
	  
	  
	  
	  private String htmlOfProof;
	  private StringBuffer nativeRepresentations = new StringBuffer(10);
	  private Engine engine;
	  private CallBacks callback;

	/**
	 * @return the nativeRepresentationList
	 */
	public String getNativeRepresentations() {
		return nativeRepresentations.toString();
	}





	/**
	 * @param nativeRepresentationList the nativeRepresentationList to set
	 */
	public void setNativeRepresentations (StringBuffer nativeRepresentations) {
		this.nativeRepresentations = nativeRepresentations;
	}





	/**
	 * @return the htmlOfProof
	 */
	public String getHtmlOfProof() {
		return htmlOfProof;
	}





	/**
	 * @param htmlOfProof the htmlOfProof to set
	 */
	public void setHtmlOfProof(String htmlOfProof) {
		this.htmlOfProof = htmlOfProof;
	}

}
